r:Rng, b:, p:|r|. (when b. p)  |r| 

latex

Definitions	x:A. B(x), t  T, when b. p, r+gp, IMonoid, |g|, 1of(t), Rng, AbGrp, Group{i}, Mon, P & Q, Prop
Lemmas	mon when wf, add grp of rng wf b, monoid p wf, grp car wf, grp op wf, grp id wf, abgrp wf, add grp of rng wf, rng car wf, bool wf, rng wf